0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 289 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 27 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
palindromeB_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3A_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3A_in_ggggg([], T332, T333, T332, T333) → reverse3A_out_ggggg([], T332, T333, T332, T333)
U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3A_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeB_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeB_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeB_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeB_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeB_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeB_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeB_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeB_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeB_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeB_in_g(.(T408, .(T407, .(T408, [])))) → palindromeB_out_g(.(T408, .(T407, .(T408, []))))
palindromeB_in_g(.(T414, .(T414, []))) → palindromeB_out_g(.(T414, .(T414, [])))
palindromeB_in_g(.(T417, [])) → palindromeB_out_g(.(T417, []))
palindromeB_in_g([]) → palindromeB_out_g([])
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
palindromeB_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3A_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3A_in_ggggg([], T332, T333, T332, T333) → reverse3A_out_ggggg([], T332, T333, T332, T333)
U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3A_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeB_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeB_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeB_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeB_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeB_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeB_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeB_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeB_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeB_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeB_in_g(.(T408, .(T407, .(T408, [])))) → palindromeB_out_g(.(T408, .(T407, .(T408, []))))
palindromeB_in_g(.(T414, .(T414, []))) → palindromeB_out_g(.(T414, .(T414, [])))
palindromeB_in_g(.(T417, [])) → palindromeB_out_g(.(T417, []))
palindromeB_in_g([]) → palindromeB_out_g([])
PALINDROMEB_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_G(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
PALINDROMEB_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → REVERSE3A_IN_GGGGG(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → U1_GGGGG(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3A_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)
palindromeB_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3A_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3A_in_ggggg([], T332, T333, T332, T333) → reverse3A_out_ggggg([], T332, T333, T332, T333)
U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3A_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeB_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeB_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeB_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeB_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeB_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeB_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeB_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeB_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeB_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeB_in_g(.(T408, .(T407, .(T408, [])))) → palindromeB_out_g(.(T408, .(T407, .(T408, []))))
palindromeB_in_g(.(T414, .(T414, []))) → palindromeB_out_g(.(T414, .(T414, [])))
palindromeB_in_g(.(T417, [])) → palindromeB_out_g(.(T417, []))
palindromeB_in_g([]) → palindromeB_out_g([])
PALINDROMEB_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_G(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
PALINDROMEB_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → REVERSE3A_IN_GGGGG(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → U1_GGGGG(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3A_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)
palindromeB_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3A_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3A_in_ggggg([], T332, T333, T332, T333) → reverse3A_out_ggggg([], T332, T333, T332, T333)
U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3A_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeB_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeB_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeB_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeB_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeB_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeB_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeB_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeB_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeB_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeB_in_g(.(T408, .(T407, .(T408, [])))) → palindromeB_out_g(.(T408, .(T407, .(T408, []))))
palindromeB_in_g(.(T414, .(T414, []))) → palindromeB_out_g(.(T414, .(T414, [])))
palindromeB_in_g(.(T417, [])) → palindromeB_out_g(.(T417, []))
palindromeB_in_g([]) → palindromeB_out_g([])
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3A_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)
palindromeB_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3A_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3A_in_ggggg([], T332, T333, T332, T333) → reverse3A_out_ggggg([], T332, T333, T332, T333)
U1_ggggg(T315, T316, T317, T318, T319, T320, reverse3A_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3A_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U2_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3A_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeB_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeB_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeB_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeB_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeB_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeB_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeB_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeB_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeB_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeB_in_g(.(T408, .(T407, .(T408, [])))) → palindromeB_out_g(.(T408, .(T407, .(T408, []))))
palindromeB_in_g(.(T414, .(T414, []))) → palindromeB_out_g(.(T414, .(T414, [])))
palindromeB_in_g(.(T417, [])) → palindromeB_out_g(.(T417, []))
palindromeB_in_g([]) → palindromeB_out_g([])
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3A_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)
REVERSE3A_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3A_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)
From the DPs we obtained the following set of size-change graphs: